Inference at * 
Iof proof for Lemma filter-commutes:


  T:Type, P1, P2:(T), L:(T List). filter(P1;filter(P2;L)) ~ filter(P2;filter(P1;L)) 

latex

 by InteriorProof ObviousListInduction 

latex

 .

Definitions	SQType(T), {T}, left + right, Unit, P  Q, P & Q, x:A  B(x), P  Q, f(a), , s = t, b, A, b, Type, , x:A. B(x), s ~ t, x:AB(x), type List, t  T
Lemmas	not assert elim, bool sq, assert elim, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf